DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2017.9

Removing Cycles from Proofs

Authors: Andrea Aler Tubella, Alessio Guglielmi, and Benjamin Ralph

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract

If we track atom occurrences in classical propositional proofs in deep inference, we see that they can form cyclic structures between cuts and identity steps. These cycles are an obstacle to a very natural form of normalisation, that simply unfolds all the contractions in a proof. This mechanism, which we call ‘decomposition’, has many points of contact with explicit substitutions in lambda calculi. In the presence of cycles, decomposition does not terminate, and this is an obvious drawback if we want to interpret proofs computationally. One way of eliminating cycles is eliminating cuts. However, we could ask ourselves whether it is possible to eliminate cycles independently of (general) cut elimination. This paper shows an efficient way to do so, therefore establishing the independence of decomposition from cut elimination. In other words, cut elimination in propositional logic can be separated into three separate procedures: 1) cycle elimination, 2) unfolding of contractions, 3) elimination of cuts in the linear fragment.

Cite as

Andrea Aler Tubella, Alessio Guglielmi, and Benjamin Ralph. Removing Cycles from Proofs. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{alertubella_et_al:LIPIcs.CSL.2017.9,
  author =	{Aler Tubella, Andrea and Guglielmi, Alessio and Ralph, Benjamin},
  title =	{{Removing Cycles from Proofs}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{9:1--9:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.9},
  URN =		{urn:nbn:de:0030-drops-77008},
  doi =		{10.4230/LIPIcs.CSL.2017.9},
  annote =	{Keywords: proof theory, deep inference, proof complexity}
}

Document

DOI: 10.4230/LIPIcs.RTA.2010.135

A Proof Calculus Which Reduces Syntactic Bureaucracy

Authors: Alessio Guglielmi, Tom Gundersen, and Michel Parigot

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract

In usual proof systems, like the sequent calculus, only a very limited way of combining proofs is available through the tree structure. We present in this paper a logic-independent proof calculus, where proofs can be freely composed by connectives, and prove its basic properties. The main advantage of this proof calculus is that it allows to avoid certain types of syntactic bureaucracy inherent to all usual proof systems, in particular the sequent calculus. Proofs in this system closely reflect their atomic flow, which traces the behaviour of atoms through structural rules. The general definition is illustrated by the standard deep-inference system for propositional logic, for which there are known rewriting techniques that achieve cut elimination based only on the information in atomic flows.

Cite as

Alessio Guglielmi, Tom Gundersen, and Michel Parigot. A Proof Calculus Which Reduces Syntactic Bureaucracy. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 135-150, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{guglielmi_et_al:LIPIcs.RTA.2010.135,
  author =	{Guglielmi, Alessio and Gundersen, Tom and Parigot, Michel},
  title =	{{A Proof Calculus Which Reduces Syntactic Bureaucracy}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{135--150},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.135},
  URN =		{urn:nbn:de:0030-drops-26490},
  doi =		{10.4230/LIPIcs.RTA.2010.135},
  annote =	{Keywords: Logic, Proof theory, Deep Inference, Flow graphs, Proof Systems, Open Deduction, Rewriting, Confluence, Termination}
}

Search Results

Documents authored by Guglielmi, Alessio

Removing Cycles from Proofs

Abstract

Cite as

A Proof Calculus Which Reduces Syntactic Bureaucracy

Abstract

Cite as

Thanks for your feedback!

Could not send message